00100	LE(X1 X2) ↔ R(D(X1 X2)O) ;
00200	LE(D(X1 X2) X1);
00300	LE( D(D(X1 X3) D(X2 X3))  D(D(X1 X2) X3) );
00400	LE(O X1);
00500	R(X1 X1);
00600	(LE(X1 X2) ∧ LE(X2 X1)) → R(X1 X2);
00700	LE(X1 U) ;;
00800	LE(X1 X2) → LE(D(X1 X3)D(X2 X3));
00850	R(D(X1 D(U X1)) D(U D(U X1)));
00900	 R(D(X1 X1) O); R(D(X1 U) O); R(D(O X1) O);
01000	∀(X1 X2 X3)( LE( X1  X2) ∧ LE( X2 X3)) → LE( X1  X3);
01100	∀(X1)R(D(X1 O) X1);∀(X1 X2 X3)(LE(D(X1 X2) X3) → LE(D(X1 X3 ) X2)); 
01200	∀(X1 X2 X3)(LE(X1 X2) → LE(D(X3 X2) D(X3 X1)));;
01250	
01300	
01400	∀(X1 X2)(R(D(U X1) D(U X2)) →R(D(U D(X1 X2)) U));;
01500	
01600	
01700